\begin{tabbing}
$\forall$\=$k$:Knd, $T$:Type, $l$:IdLnk, ${\it ds}$,${\it dt}$:fpf(Id; ${\it tg}$.Type),\+
\\[0ex]$g$:((${\it tg}$:Id $\times$ (decl{-}state(${\it ds}$)$\rightarrow$$T$$\rightarrow$(decl{-}type\{i:l\}(${\it dt}$; ${\it tg}$) List))) List).
\-\\[0ex](($\uparrow$isrcv($k$))
\\[0ex]$\Rightarrow$ \=((destination(lnk($k$)) = source($l$) $\in$ Id)\+
\\[0ex]$\wedge$ (($\uparrow$eq\_lnk(lnk($k$); $l$)) $\Rightarrow$ ($T$ = decl{-}type\{i:l\}(${\it dt}$; tag($k$))))))
\-\\[0ex]$\Rightarrow$ normal{-}ds\=\{i:l\}\+
\\[0ex](${\it ds}$)
\-\\[0ex]$\Rightarrow$ normal{-}type\=\{i:l\}\+
\\[0ex]($T$)
\-\\[0ex]$\Rightarrow$ normal{-}ds\=\{i:l\}\+
\\[0ex](${\it dt}$)
\-\\[0ex]$\Rightarrow$ R{-}realizes\=\{i:l\}\+
\\[0ex](Rsends(${\it ds}$; $k$; $T$; $l$; ${\it dt}$; $g$); ${\it es}$.sends{-}p(${\it es}$; ${\it ds}$; $k$; $T$; $l$; ${\it dt}$; $g$))
\-
\end{tabbing}